\begin{tabbing}
for\= clients $C$ sends FIFO\+
\\[0ex]from j to i via ($S$[j,i],${\it codes}$)
\\[0ex]receives at i via ($R$[i],${\it decodes}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:$C$.\+
\\[0ex]$\exists$\=$f$:\{$e$:E$\mid$ $R$($i$,$e$)\} $\rightarrow$\{$e$:E$\mid$ $\exists$$j$:$C$. ($S$($j$,$i$,$e$))\} \+
\\[0ex]($\lambda$$e$.$\exists$$j$:$C$. ($S$($j$,$i$,$e$)) $\leftarrow\leftarrow$ $f$$--$ $\lambda$$e$.$R$($i$,$e$)
\\[0ex]\& (\=$\forall$$e$:\{$e$:E$\mid$ $R$($i$,$e$)\} , $j$:\{$j$:$C$$\mid$ $S$($j$,$i$,$f$($e$))\} .\+
\\[0ex]${\it decodes}$($i$,$e$,(state when $e$)) = ${\it codes}$($j$,$i$,$f$($e$),(state when $f$($e$))))
\-\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ $R$($i$,$e$)\} , $j$:$C$.\+
\\[0ex]($S$($j$,$i$,$f$($e$))) $\Rightarrow$ ($S$($j$,$i$,$f$(${\it e'}$))) $\Rightarrow$ $f$($e$) c$\leq$ $f$(${\it e'}$) $\Rightarrow$ $e$ c$\leq$ ${\it e'}$))
\-\-\-
\end{tabbing}